This error is strange.

Error: The variable truncn was not found in the current environment.

Why was truncn not found? I can certainly find truncn in archimedean.v.

This error is strange.

Error: The variable truncn was not found in the current environment.

Why was truncn not found? I can certainly find truncn in archimedean.v.

It might be because the CI is testing with the previous version of MathComp (2.3.0) in which there was no truncn.

Thank you for the comment.
Then I think the pull request went well, but please tell me if I need to fix something.

@affeldt-aist Would it be possible to review this pull request?

I have introduced a tentative structure Cumulative01 that carries the proofs that the function tends to 0 in -oo and to 1 in +oo. This way we can put the HB declaration that the Lebesgue-Stieltjes measure of such a function is a probability measure in lebesgue_stieltjes_measure.v and cdf_lebesgue_stieltjes_id still type-checks. (fyi: @CohenCyril )

TODO: write documentation and changelog for Cumulative01 if deemed useful.

@affeldt-aist
Thank you very much for the review.
I'd prefer to generalize 0 and 1, something like

HB.mixin Record isCumulativeBdd (R : numFieldType) (l u : R) (f : R -> R) := {
  cumulativeNyl : f @ -oo --> (l:R) ;
  cumulativeyu : f @ +oo --> (u:R) }.

#[short(type=cumulativeBdd)]
HB.structure Definition CumulativeBdd (R : numFieldType) (l u : R) :=
  { f of isCumulativeBdd R l u f & Cumulative R f}.

Arguments cumulativeNyl {R} l u s.
Arguments cumulativeyu {R} l u s.

Section probability_measure_of_lebesgue_stieltjes_mesure.
Context {R : realType} (f : @cumulativeBdd R 0 1).

But it's up to you, because 0 and 1 are sufficient for the time being.

If think that it is ok to merge since the work will anyway continue with issue #1572 . @CohenCyril any thought?

Thank you for the review and the merge.